Spec Sharp

Spec#
Paradigm(s) multi-paradigm: structured, imperative, object-oriented, event-driven, functional, contract
Appeared in 2004
Designed by Microsoft Research
Developer Microsoft Research
Stable release 1.0.21125
Typing discipline static, strong, safe, nominative
Influenced by C#, Eiffel
Influenced Sing#
Website Spec# website

Spec# is a programming language with specification language features that extends the capabilities of the C# programming language with Eiffel-like contracts, including object invariants, preconditions and postconditions. Like ESC/Java, it includes a static checking tool based on a theorem prover that is able to statically verify many of these invariants. It also includes a variety of other minor extensions to the language, such as non-null reference types.

The code contracts API in the .NET Framework 4.0 has evolved with Spec#.

Microsoft Research developed both Spec# and C#; in turn, Spec# serves as the foundation of the Sing# programming language, which Microsoft Research also developed.

Contents

Features

See also: Spec# in C Sharp syntax.

Spec# extends the core C# programming language with features such as:

Example

This example shows two of the basic structures that are used when adding contracts to your code (try Spec# in your browser).

    static void Main(string![] args)
        requires args.Length > 0;
    {
        foreach(string arg in args)
        {
            Console.WriteLine(arg);
        }
    }

Sources

See also

External links